Nuprl Definition : qadd_grp 11,40

qadd_grp == <rationals, x,y. qeq(xy), x,y. q_le(xy), x,yx + y, 0, x.-(x)> 
latex



clarification:

qadd_grp == <rationals, x,y. qeq(xy), x,y. q_le(xy), x,yx + y, 0, x.(-1) * x
latex


Definitionsrationals, qeq(rs), q_le(rs), r + s, <ab>, x.A(x), r * s, -n, #$n
FDL editor aliasesqadd_grp

origin